Validation of array accesses: integration of flow analysis and program verification techniques

1997 ◽  
Vol 7 (4) ◽  
pp. 201-227
Author(s):  
Raymond W. Lo ◽  
Karl N. Levitt ◽  
Ronald A. Olsson
Keyword(s):  
Program Verification ◽  
Flow Analysis ◽  
Verification Techniques

A REVIEW APPROACH TO DETECTING VIOLATIONS OF CONSISTENCY BETWEEN SPECIFICATION AND PROGRAM STRUCTURES

2008 ◽  
Vol 18 (08) ◽  
pp. 1013-1042
Author(s):  
YUTING CHEN ◽  
SHAOYING LIU ◽  
W. ERIC WONG
Keyword(s):  
Program Verification ◽  
Formal Proof ◽  
Black Box ◽  
Program Review ◽  
Prototype Tool ◽  
Essential Idea ◽  
Black Box Testing ◽  
Structural Consistency ◽  
Verification Techniques

The application of specification-based program verification techniques (e.g., black-box testing, formal proof) faces strong challenges in practice when the gap between the structure of a specification and that of its program is large. This paper describes a view-based program review approach to addressing these challenges. The essential idea of the approach is first to derive comparable views from the specification and program, and then detect and eliminate the violations of structural consistency in the program views on the basis of a set of criteria. We also developed a prototype tool to support the review approach, and conducted a case study to assess the effectiveness of the approach.

Program Verification Techniques Based on Separation Logic

2009 ◽  
Vol 20 (8) ◽  
pp. 2051-2061 ◽  
Author(s):  
Da-Ming HUANG ◽  
Qing-Kai ZENG
Keyword(s):  
Program Verification ◽  
Separation Logic ◽  
Verification Techniques

scholarly journals Formal Verification of Real-Time Systems with Data Processing

2017 ◽  
Vol 61 (2) ◽  
pp. 166
Author(s):  
Tamás Tóth ◽  
István Majzik
Keyword(s):  
Real Time ◽  
Program Verification ◽  
Data Flow ◽  
Timed Automata ◽  
Formal Analysis ◽  
Time Behavior ◽  
Real Time Systems ◽  
Critical Systems ◽  
Time Systems ◽  
Verification Techniques

The behavior of practical safety critical systems often combines real-time behavior with structured data flow. To ensure correctness of such systems, both aspects have to be modeled and formally verified. Time related behavior can be efficiently modeled and analyzed in terms of timed automata. At the same time, program verification techniques like abstract interpretation and software model checking can efficiently handle data flow. In this paper, we describe a simple formalism that represents both aspects of such systems in a uniform and explicit way, thus enables the combination of formal analysis methods for real-time systems and software using standard techniques.

Panellist position statement: some industrial experience with program verification

2005 ◽  
Vol 363 (1835) ◽  
pp. 2393-2394
Author(s):  
Roderick Chapman
Keyword(s):  
Software Engineering ◽  
Formal Methods ◽  
Programming Language ◽  
Program Verification ◽  
Position Statement ◽  
Software Systems ◽  
Engineering Company ◽  
Verification Tools ◽  
High Integrity ◽  
Verification Techniques

As the only obvious ‘industrial’ member of the panel, I would like to introduce myself and the work I am involved with. Praxis is a practising software engineering company that is well known for applying so-called ‘Formal Methods’ in the development of high-integrity software system. We are also responsible for the Spark programming language and verification tools ( John Barnes with Praxis High Integrity Systems 2003 ). Spark remains one of the very few technologies to offer a sound verification system for an industrially usable imperative programming language. Despite the popular belief that ‘no one does formal methods’, we (and our customers) regularly employ strong verification techniques on industrial-scale software systems. I would like to address three main points:

Sign in / Sign up

Export Citation Format

Share Document